Nuprl Lemma : predicate_equivalent_implies 11,40
T:Type, P1, P2:(TType). P1  P2  (P1  P2 & P2  P1) 
latex

Definitionst  T, Type, x:AB(x), x:A  B(x), f(a), P  Q, x:A. B(x), P  Q, P & Q, P  Q, A c B, P1  P2, P1  P2

origin